Inference at * 1 1 4 2 
Iof proof for Lemma gen hyp tp:



1. A : Type
2. e : A
3. H : AType
4. x:A. (e = x)
5. z : H(e)
6. A  Type
7. e  A
8. x:A. (e = x)  Type
  z  0 

latex

 by (\p.D (get_int_arg `i` p) p) 

latex

 1: 

 1: 4. x : A
 1: 5. e = x
 1: 6. z : H(e)
 1: 7. A  Type
 1: 8. e  A
 1: 9. x:A. (e = x)  Type
 1:   z  0
 .

Definitions

x:A. B(x)